/*
 * This file is part of the openHiTLS project.
 *
 * openHiTLS is licensed under the Mulan PSL v2.
 * You can use this software according to the terms and conditions of the Mulan PSL v2.
 * You may obtain a copy of Mulan PSL v2 at:
 *
 *     http://license.coscl.org.cn/MulanPSL2
 *
 * THIS SOFTWARE IS PROVIDED ON AN "AS IS" BASIS, WITHOUT WARRANTIES OF ANY KIND,
 * EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO NON-INFRINGEMENT,
 * MERCHANTABILITY OR FIT FOR A PARTICULAR PURPOSE.
 * See the Mulan PSL v2 for more details.
 */
#ifndef GHOST_SM4_SPEC_H
#define GHOST_SM4_SPEC_H

#include "crypt_sm4.h" // 引入 CRYPT_SM4_Ctx 等类型定义
/*@
 logic unsigned char spec_sbox_lookup(integer i) = (unsigned char)(
    i == 0x00 ? 0xd6 : i == 0x01 ? 0x90 : i == 0x02 ? 0xe9 : i == 0x03 ? 0xfe :
    i == 0x04 ? 0xcc : i == 0x05 ? 0xe1 : i == 0x06 ? 0x3d : i == 0x07 ? 0xb7 :
    i == 0x08 ? 0x16 : i == 0x09 ? 0xb6 : i == 0x0a ? 0x14 : i == 0x0b ? 0xc2 :
    i == 0x0c ? 0x28 : i == 0x0d ? 0xfb : i == 0x0e ? 0x2c : i == 0x0f ? 0x05 :
    i == 0x10 ? 0x2b : i == 0x11 ? 0x67 : i == 0x12 ? 0x9a : i == 0x13 ? 0x76 :
    i == 0x14 ? 0x2a : i == 0x15 ? 0xbe : i == 0x16 ? 0x04 : i == 0x17 ? 0xc3 :
    i == 0x18 ? 0xaa : i == 0x19 ? 0x44 : i == 0x1a ? 0x13 : i == 0x1b ? 0x26 :
    i == 0x1c ? 0x49 : i == 0x1d ? 0x86 : i == 0x1e ? 0x06 : i == 0x1f ? 0x99 :
    i == 0x20 ? 0x9c : i == 0x21 ? 0x42 : i == 0x22 ? 0x50 : i == 0x23 ? 0xf4 :
    i == 0x24 ? 0x91 : i == 0x25 ? 0xef : i == 0x26 ? 0x98 : i == 0x27 ? 0x7a :
    i == 0x28 ? 0x33 : i == 0x29 ? 0x54 : i == 0x2a ? 0x0b : i == 0x2b ? 0x43 :
    i == 0x2c ? 0xed : i == 0x2d ? 0xcf : i == 0x2e ? 0xac : i == 0x2f ? 0x62 :
    i == 0x30 ? 0xe4 : i == 0x31 ? 0xb3 : i == 0x32 ? 0x1c : i == 0x33 ? 0xa9 :
    i == 0x34 ? 0xc9 : i == 0x35 ? 0x08 : i == 0x36 ? 0xe8 : i == 0x37 ? 0x95 :
    i == 0x38 ? 0x80 : i == 0x39 ? 0xdf : i == 0x3a ? 0x94 : i == 0x3b ? 0xfa :
    i == 0x3c ? 0x75 : i == 0x3d ? 0x8f : i == 0x3e ? 0x3f : i == 0x3f ? 0xa6 :
    i == 0x40 ? 0x47 : i == 0x41 ? 0x07 : i == 0x42 ? 0xa7 : i == 0x43 ? 0xfc :
    i == 0x44 ? 0xf3 : i == 0x45 ? 0x73 : i == 0x46 ? 0x17 : i == 0x47 ? 0xba :
    i == 0x48 ? 0x83 : i == 0x49 ? 0x59 : i == 0x4a ? 0x3c : i == 0x4b ? 0x19 :
    i == 0x4c ? 0xe6 : i == 0x4d ? 0x85 : i == 0x4e ? 0x4f : i == 0x4f ? 0xa8 :
    i == 0x50 ? 0x68 : i == 0x51 ? 0x6b : i == 0x52 ? 0x81 : i == 0x53 ? 0xb2 :
    i == 0x54 ? 0x71 : i == 0x55 ? 0x64 : i == 0x56 ? 0xda : i == 0x57 ? 0x8b :
    i == 0x58 ? 0xf8 : i == 0x59 ? 0xeb : i == 0x5a ? 0x0f : i == 0x5b ? 0x4b :
    i == 0x5c ? 0x70 : i == 0x5d ? 0x56 : i == 0x5e ? 0x9d : i == 0x5f ? 0x35 :
    i == 0x60 ? 0x1e : i == 0x61 ? 0x24 : i == 0x62 ? 0x0e : i == 0x63 ? 0x5e :
    i == 0x64 ? 0x63 : i == 0x65 ? 0x58 : i == 0x66 ? 0xd1 : i == 0x67 ? 0xa2 :
    i == 0x68 ? 0x25 : i == 0x69 ? 0x22 : i == 0x6a ? 0x7c : i == 0x6b ? 0x3b :
    i == 0x6c ? 0x01 : i == 0x6d ? 0x21 : i == 0x6e ? 0x78 : i == 0x6f ? 0x87 :
    i == 0x70 ? 0xd4 : i == 0x71 ? 0x00 : i == 0x72 ? 0x46 : i == 0x73 ? 0x57 :
    i == 0x74 ? 0x9f : i == 0x75 ? 0xd3 : i == 0x76 ? 0x27 : i == 0x77 ? 0x52 :
    i == 0x78 ? 0x4c : i == 0x79 ? 0x36 : i == 0x7a ? 0x02 : i == 0x7b ? 0xe7 :
    i == 0x7c ? 0xa0 : i == 0x7d ? 0xc4 : i == 0x7e ? 0xc8 : i == 0x7f ? 0x9e :
    i == 0x80 ? 0xea : i == 0x81 ? 0xbf : i == 0x82 ? 0x8a : i == 0x83 ? 0xd2 :
    i == 0x84 ? 0x40 : i == 0x85 ? 0xc7 : i == 0x86 ? 0x38 : i == 0x87 ? 0xb5 :
    i == 0x88 ? 0xa3 : i == 0x89 ? 0xf7 : i == 0x8a ? 0xf2 : i == 0x8b ? 0xce :
    i == 0x8c ? 0xf9 : i == 0x8d ? 0x61 : i == 0x8e ? 0x15 : i == 0x8f ? 0xa1 :
    i == 0x90 ? 0xe0 : i == 0x91 ? 0xae : i == 0x92 ? 0x5d : i == 0x93 ? 0xa4 :
    i == 0x94 ? 0x9b : i == 0x95 ? 0x34 : i == 0x96 ? 0x1a : i == 0x97 ? 0x55 :
    i == 0x98 ? 0xad : i == 0x99 ? 0x93 : i == 0x9a ? 0x32 : i == 0x9b ? 0x30 :
    i == 0x9c ? 0xf5 : i == 0x9d ? 0x8c : i == 0x9e ? 0xb1 : i == 0x9f ? 0xe3 :
    i == 0xa0 ? 0x1d : i == 0xa1 ? 0xf6 : i == 0xa2 ? 0xe2 : i == 0xa3 ? 0x2e :
    i == 0xa4 ? 0x82 : i == 0xa5 ? 0x66 : i == 0xa6 ? 0xca : i == 0xa7 ? 0x60 :
    i == 0xa8 ? 0xc0 : i == 0xa9 ? 0x29 : i == 0xaa ? 0x23 : i == 0xab ? 0xab :
    i == 0xac ? 0x0d : i == 0xad ? 0x53 : i == 0xae ? 0x4e : i == 0xaf ? 0x6f :
    i == 0xb0 ? 0xd5 : i == 0xb1 ? 0xdb : i == 0xb2 ? 0x37 : i == 0xb3 ? 0x45 :
    i == 0xb4 ? 0xde : i == 0xb5 ? 0xfd : i == 0xb6 ? 0x8e : i == 0xb7 ? 0x2f :
    i == 0xb8 ? 0x03 : i == 0xb9 ? 0xff : i == 0xba ? 0x6a : i == 0xbb ? 0x72 :
    i == 0xbc ? 0x6d : i == 0xbd ? 0x6c : i == 0xbe ? 0x5b : i == 0xbf ? 0x51 :
    i == 0xc0 ? 0x8d : i == 0xc1 ? 0x1b : i == 0xc2 ? 0xaf : i == 0xc3 ? 0x92 :
    i == 0xc4 ? 0xbb : i == 0xc5 ? 0xdd : i == 0xc6 ? 0xbc : i == 0xc7 ? 0x7f :
    i == 0xc8 ? 0x11 : i == 0xc9 ? 0xd9 : i == 0xca ? 0x5c : i == 0xcb ? 0x41 :
    i == 0xcc ? 0x1f : i == 0xcd ? 0x10 : i == 0xce ? 0x5a : i == 0xcf ? 0xd8 :
    i == 0xd0 ? 0x0a : i == 0xd1 ? 0xc1 : i == 0xd2 ? 0x31 : i == 0xd3 ? 0x88 :
    i == 0xd4 ? 0xa5 : i == 0xd5 ? 0xcd : i == 0xd6 ? 0x7b : i == 0xd7 ? 0xbd :
    i == 0xd8 ? 0x2d : i == 0xd9 ? 0x74 : i == 0xda ? 0xd0 : i == 0xdb ? 0x12 :
    i == 0xdc ? 0xb8 : i == 0xdd ? 0xe5 : i == 0xde ? 0xb4 : i == 0xdf ? 0xb0 :
    i == 0xe0 ? 0x89 : i == 0xe1 ? 0x69 : i == 0xe2 ? 0x97 : i == 0xe3 ? 0x4a :
    i == 0xe4 ? 0x0c : i == 0xe5 ? 0x96 : i == 0xe6 ? 0x77 : i == 0xe7 ? 0x7e :
    i == 0xe8 ? 0x65 : i == 0xe9 ? 0xb9 : i == 0xea ? 0xf1 : i == 0xeb ? 0x09 :
    i == 0xec ? 0xc5 : i == 0xed ? 0x6e : i == 0xee ? 0xc6 : i == 0xef ? 0x84 :
    i == 0xf0 ? 0x18 : i == 0xf1 ? 0xf0 : i == 0xf2 ? 0x7d : i == 0xf3 ? 0xec :
    i == 0xf4 ? 0x3a : i == 0xf5 ? 0xdc : i == 0xf6 ? 0x4d : i == 0xf7 ? 0x20 :
    i == 0xf8 ? 0x79 : i == 0xf9 ? 0xee : i == 0xfa ? 0x5f : i == 0xfb ? 0x3e :
    i == 0xfc ? 0xd7 : i == 0xfd ? 0xcb : i == 0xfe ? 0x39 : i == 0xff ? 0x48 : 0x00);

  // 32位循环左移
  logic integer ROTL(integer x, integer n) =
    ((x << n) | (x >> (32 - n))) & 0xFFFFFFFF;

  // L
  logic uint32_t L_transform(uint32_t b) =
  (uint32_t)(b ^ ROTL(b, 2) ^ ROTL(b, 10) ^ ROTL(b, 18) ^ ROTL(b, 24));

  // τ
  logic uint32_t T_transform(uint32_t val) = L_transform(
    (uint32_t) ( // Add outer cast here
      (uint32_t)spec_sbox_lookup((val >> 24) & 0xFF) << 24 |
      (uint32_t)spec_sbox_lookup((val >> 16) & 0xFF) << 16 |
      (uint32_t)spec_sbox_lookup((val >>  8) & 0xFF) <<  8 |
      (uint32_t)spec_sbox_lookup( val        & 0xFF))
  );

  // L'
  logic uint32_t L_prime_transform(uint32_t b) = (uint32_t)(b ^ ROTL(b, 13) ^ ROTL(b, 23));

  // τ'
  logic uint32_t K_tau_transform(uint32_t val) =
    L_prime_transform((uint32_t)(
      (uint32_t)spec_sbox_lookup((val >> 24) & 0xFF) << 24 |
      (uint32_t)spec_sbox_lookup((val >> 16) & 0xFF) << 16 |
      (uint32_t)spec_sbox_lookup((val >>  8) & 0xFF) <<  8 |
      (uint32_t)spec_sbox_lookup( val        & 0xFF)
    ));

  // SM4 常量与查找表的公理化模型
  axiomatic SM4_Constants {
    // 模拟密钥扩展中使用的 KBOX 查表
    logic uint32_t KBOX_lookup(integer i);

    // 模拟加解密中使用的 XBOX 查表
    logic uint32_t XBOX_lookup(integer table_num, integer i);

    // 模拟系统参数 FK 和固定参数 CK
    logic uint32_t FK_lookup(integer i);
    logic uint32_t CK_lookup(integer i);
  }

  // SM4 密钥扩展算法的公理化模型
  axiomatic SM4_KeySchedule {

    // 递归定义第 i 个轮密钥 (0 <= i < 32)
    logic uint32_t spec_sm4_round_key(uint8_t* key, integer i);

    // 定义前4个轮密钥的生成规则 (由主密钥和FK异或得到)
    axiom key_round_base:
      \forall uint8_t* key, integer i; 0 <= i < 4 ==>
        spec_sm4_round_key(key, i) ==
          ( ((uint32_t)key[4*i]<<24 | (uint32_t)key[4*i+1]<<16 | (uint32_t)key[4*i+2]<<8 | key[4*i+3]) ^ FK_lookup(i) );

    // 定义后续轮密钥的递归生成规则
    axiom key_round_inductive:
      \forall uint8_t* key, integer i; 4 <= i < 32 ==>
        spec_sm4_round_key(key, i) == (spec_sm4_round_key(key, i-4) ^
          K_tau_transform((uint32_t)(spec_sm4_round_key(key, i-3) ^ spec_sm4_round_key(key, i-2) ^ spec_sm4_round_key(key, i-1) ^ CK_lookup(i-4))));
  }

  axiomatic SM4_Cipher {

    // 模拟一轮 SM4 加密函数 F
    logic uint32_t spec_sm4_round(uint32_t x0, uint32_t x1, uint32_t x2, uint32_t x3, uint32_t rk);

    // 32轮 SM4 单块加密
    logic void* spec_sm4_encrypt_block(uint8_t* input, uint32_t* round_keys);

    // 32轮 SM4 单块解密
    logic void* spec_sm4_decrypt_block(uint8_t* input, uint32_t* round_keys);
  }

*/

#endif // GHOST_SM4_SPEC_H